window.onload=function(){ 
	var rev = "$Revision: 191 $"; 
	rev = rev.replace(/\$/g , '');
	document.getElementById("revision").innerHTML =  rev; 
}